T:Type, L:(T List). L  []  (L = []) 

latex

Definitions	, t  T, P  Q, P  Q, P & Q, P  Q, x:A. B(x), True, Y, ||as||
Lemmas	length sublist, length zero, non neg length, length wf1, sublist wf, nil sublist